$\forall$$A$, $B$:Type, ${\it es}$:ES, $X$:AbsInterface($A$ + $B$). es{-}interface{-}left($X$) $\in$ AbsInterface($A$)